Nuprl Lemma : int_add_grp_wf 13,42

<+>  AbGrp{1} 
latex


Upgroups 1
Definitions of Statement|g|, *, Mon, Group{i}, AbGrp, <+>
Definitions<+>, AbGrp, t  T, P & Q, xt(x), P  Q, , P  Q, x f y, P  Q, x:AB(x), IsEqFun(T;eq), Assoc(T;op), Ident(T;op;id), Inverse(T;op;id;inv), t.2, t.1, *, |g|, Comm(T;op), Mon, Group{i}, x(s)
Lemmasgrp op wf, grp car wf, comm wf, le int wf, eq int wf, mk grp, assert of eq int, iff functionality wrt iff, assert wf, iff wf, all functionality wrt iff

origin